Katara: Synthesizing CRDTs with Verified Lifting
Replicated data types (RDTs) such as CRDTs are becoming increasingly popular as a simplified way for programming distributed systems. RDTs are local data structures with a familiar interface (such as sets, lists, trees) that can automatically synchronize data between multiple devices in the background. Even though RDTs are often considered to be simpler to implement than other approaches to eventual consistency, the construction of correct RDTs is still difficult and error-prone. Instead of writing the implementations of RDTs by hand, an alternative idea is to synthesize RDT implementations from a regular "sequential" data type and additional user-provided annotations. This process is called lifting. To ensure correctness of the syntesized RDT implementation, the correctness properties are encoded using SMT logic and are automatically verified during synthesis.
For this seminar topic, you will look into how Katara synthesises RDTs. You will touch topics both in the area of consistency in distributed systems (i.e., CRDTs), as well as program synthesis and to some extent also verification.